perm filename FIRST.NEW[W77,JMC]3 blob sn#275646 filedate 1977-04-09 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00012 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 00003	.bb "#. Recursive Programs."
C00010 00004	.bb "#. The Functional Equation of a Recursive Program."
C00015 00005	.bb "#. First Order Axioms for Lisp."
C00023 00006	.bb "#. An Extended Example."
C00033 00007	.bb "#. The Minimization Schema."
C00040 00008	.bb "#. Proof Methods as Axiom Schemata"
C00048 00009	.bb "#. Representations Using Finite Approximations."
C00060 00010	.BB "#. Questions of Incompleteness."
C00067 00011	.bb "#. References."
C00070 00012	.skip 1
C00071 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.every heading (REPRESENTATION,...draft...,{page})
.font B "zero30"
.AT "qt" ⊂"%At%*"⊃
.AT "qw" ⊂"%Aw%*"⊃
.at "Goedel" ⊂"G%B:%*odel"⊃
.skip 15

.cb REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

.cb by John McCarthy
.skip 10


	This paper presents methods of representing recursive programs by
sentences and schemata of first order logic, characterization of
%2recursion induction%1, %2subgoal induction%1, %2inductive assertions%1
and other ways of proving facts about programs as axiom schemata of first
order logic, and applications of these results to proving assertions about
programs.


.skip to column 1
.bb "#. Introduction and Motivation."

	It has been concluded from the undecideability of both equivalence
and non-equivalence of abstract recursive program schemata that recursive
programs cannot be characterized in first order logic.  Cooper (1969)
showed how to characterize them in second order logic, and that seemed to
settle the matter.  However, we will exhibit first order characterizations
that are incomplete only in that they admit non-standard models like those
of first order arithmetic.  It now seems likely that all "ordinary"
assertions about programs will be provable or disprovable in first order
theories.

	Beyond illuminating the logical structure of computer programs,
these results have some practical significance.  First, the correctness of
a computer program often involves facts about other mathematical domains,
and these are often conveniently expressed in first order logic or in a
set theory axiomatized in first order logic.  It has proved particularly
difficult to work within logics that admit only continuous functions and
predicates.  Second, proof-checking and theorem proving programs have been
developed for first order logic.  Finally, first order logic is complete,
so that the Goedelian incompleteness of any theory is in the set of axioms
and can be reduced when necessary by adding axioms rather than by changing
the logical system.

	While our goal is first order representations of recursive
programs, we will make considerable informal use of higher order
functionals and predicates.

	We present two methods of representing recursive programs.  The
first involves a %2functional equation%1 and a %2minimization schema%1 for
each program.  The functional equation has the function on both sides of
an equality sign and so defines it implicitly.  However, all variables are
universally quantified.  The second approach defines the function
explicitly, but existential quantifiers asserting the existence of finite
approximations to the function occur in the formula.  The fact that the
functional equation of a program not known to terminate can nevertheless
be written so simply in first order logic was first discovered by
Cartwright (1977), but the remaining results seem to be new.


.bb "#. Recursive Programs."

	An adequate background for this paper is contained in (Manna 1974)
and more concisely in (Manna, Ness and Vuillemin 1973).  The connections
of recursive programs with second order logic are given in (Cooper 1969)
and (Park 1970).

	We shall consider mainly %2recursive programs%1 of the general form

!!g1:	%2f(x) ← %At%*[f](x)%1,

where %At%* is a %2computable functional%1 like

!!g2:	%2%At%* = λf.λx.(qif x = 0 qthen 1 qelse x . f(x - 1))%1,

which gives rise to the well known recursive definition of the factorial
function, namely

!!g3:	%2n! ← qif n = 0 qthen 1 qelse n . (n - 1)!%1.

	In general, we shall be interested in partial functions from a
domain D1 to a domain D2, and it will often be necessary to augment these
domains by an undefined element denoted by %Aw%* giving rise to domains D1%5+%*
and D2%5+%*.  A set ⊗F of total base functions on the domains is assumed
available, and we study functions %2computable in the set F%1. 

	It is important to distinguish between a program as a text
and the partial function defined by the program
when one is interested in describing the dependence of the function on
the interpretation of the basic function and predicate symbols.  However,
we will be working with just one interpretation at a time, so we won't use
separate symbols for programs and the functions they determine.
.bb "#. The Functional Equation of a Recursive Program."

	Consider the Lisp program

!!h1:	%2subst[x,y,z] ← qif qat z qthen [qif z=y qthen x qelse z]
qelse subst[x,y,qa z] . subst[x,y,qd z]%1.

The above is in Lisp %2external%1 or %2publication%1 notation in
which _qa_%2x%1_ (bold face qa) stands for %2car[x]%1,
_qd_%2x%1_ for %2cdr[x]%1, _%2x_._y%1_
for %2cons[x,y]%1, _qat_%2x%1_ for %2atom[x]%1, _qn_%2x%1_ for %2null[x]%1, and
%2<x%41%2 ... x%4n%1> for %2list[x%41%2, ... ,x%4n%1], and
%2x_*_y%1 for %2append[x,y]%1.  Equality is taken as equality of
S-expressions so that qeq is not used.  The program is written

	(DE SUBST (X Y Z) (COND ((ATOM Z) (COND ((EQUAL Z Y) X) (T Z)))
(T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

in Lisp %2internal notation%1.

	The basic functions α{%2car, cdr, cons, atomα}%1 of Lisp are all
assumed total, but we will say nothing about the values of ⊗car and
⊗cdr when applied to atoms.  According to the fixed point theory of
recursive programs, this program defines a function from ⊗Sexp (the
set of S-expressions) to Sexp%5+%* (the set of S-expressions augmented
by %Aw%*).  This function can be computed by any %2safe computation rule%1,
(in the terminology of Manna, Ness, and Vuillemin (1973)),
and when the computation terminates, its value will belong to ⊗Sexp.  When
the computation doesn't terminate, the value of ⊗f(x) is %Aw%*.  While
the particular function %2subst%1 always terminates, we do not assume it
in writing our first order formula.  Indeed we can use the first order
formula to prove by structural induction that %2subst%1 is total.

	These facts show that the function %2subst%1 defined recursively
by ({eq h1}) satisfies the sentence

!!h2:	%2∀x y z.(subst(x,y,z) = qif qat z qthen (qif z = y qthen x qelse z)
qelse subst(x,y,qa z) . subst(x,y,qd z))%1

of first order logic.  The variables %2x, y%1 and %2z%1 range over ⊗Sexp; 
when we want to quantify over %2Sexp%5+%1, we use %2X, Y %1and%2 Z%1.
Moreover, we are augmenting first order logic
(as described in (Manna 1975))
by allowing conditional
expressions as terms.  The augmentation is does not change what
can be expressed in first order logic, because
conditional expressions can always be eliminated from sentences by
distributing predicates over them.  Thus ({eq h2}) can be written

!!h3:	%2∀x y z.(qat z ⊃ (z=y ⊃ subst(x,y,z) = x) ∧ z≠y ⊃ subst(x,y,z) = z)
∧ ¬qat z ⊃ subst(x,y,z) = subst(x,y,qa z) . subst(x,y,qd z)),%1

but we will use conditional expressions, because they are clearer and
express the content of the recursive program directly.  In fact, we recommend
their admission as terms in logic generally, and first order logic in
particular.  They don't extend the logical power, but they permit many
facts to be expressed without circumlocution.

	One goal of our first order representation is to use ({eq h1})
only to justify writing ({eq h2}) and then prove all properties of
%2subst%1 using a first order axiomatization of Lisp.
.skip 2

.bb "#. First Order Axioms for Lisp."

	We use lower case variables ⊗x, ⊗y, and ⊗z with or without
subscripts to range over S-expressions.  Capitalized variables
range over all entities.  We also use variables ⊗u, ⊗v and ⊗w with
or without subscripts to range over lists, i.e. S-expressions
such that successive %2cdr%1s eventually reach NIL.  (The %2car%1 of
a list is not required to be a list).  We use predicates %2issexp%1
and %2islist%1 to assert that an individual is an S-expression or
a list.  First come the "housekeeping" and "algebraic" axioms:

L1:	%2∀x.issexp x%1

L2:	%2∀u.islist u%1

L3:	%2∀u.issexp u%1

L4:	%2¬issexp %Aw%1

L5:	%2islist %1NIL

L6:	%2qat qNIL%1

L7:	%2∀u.(qat u ⊃ u = qnil)%1

L8:	%2∀x y.issexp (x.y)%1

L9:	%2∀x u.islist (x.u)%1

L10:	%2∀x. ¬qat x ⊃ issexp qa x%1

L11:	%2∀x. ¬qat x ⊃ issexp qd x%1

L12:	%2∀u. u ≠ qNIL ⊃ islist qd u%1

L13:	%2∀x y. qa (x.y) = x%1

L14:	%2∀x y. qd (x.y) = y%1

L15:	%2∀x y. ¬qat (x.y)%1

L16:	%2∀x.¬qat x ⊃ (qa x . qd x) = x%1

	Next we have axiom schemata of induction

LS1:	%2(∀x.qat x ⊃ %AF%* x) ∧ ∀x.(¬qat x ∧ %AF%* qa x ∧ %AF%* qd x ⊃ %AF%* x) ⊃ ∀x.%AF%* x%1

LS2:	%2(∀u.u = qnil ⊃ %AF%* u) ∧ ∀u.(u ≠ qnil ∧ %AF%* qd u ⊃ %AF%* u) ⊃ ∀u. %AF%* u%1.

	From these axioms and schemata, we can prove

!!h4:	%2∀x y z.issexp subst(x,y,z)%1

which is our way of saying that %2subst%1 is total.
The key step is applying the axiom schema LS1 with the
predicate %2%AF%*(z) ≡ issexp(x,y,z)%1.
We can also prove
in first order logic
such algebraic properties of %2subst%1 as

!!h5:	%2∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) =
subst(x,y,subst(z,y1,z1)))%1

if we have suitable axiomatization of the predicate %2occur(x,y)%1 meaning
that the atom ⊗x occurs in the S-expression ⊗y. 

	The axiomatization of the predicate %2occur%1 raises some new
problems.  It is defined by the recursive Lisp program

!!h6:	%2occur(x,y) ← (x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y)))%1.

If we were sure in advance that %2occur%1 were total, we could translate
the recursion ({eq h6}) into the sentence

!!h7:	%2∀x y.(occur(x,y) ≡
(x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y))))%1

which will suffice for proving ({eq h5}), but we
have no right to write it down from the recursive definition ({eq h6}).

	What we may write without proving that %2occur%1 is total
is an implicit definition

!!h8:	%2∀x y.(occura(x,y) =
(x equals y) or (not atom y and (occura(x,qa y) or occura(x,qd y))))%1

and

!!h9:	%2∀x y.(occur(x,y) ≡ (occura(x,y) = T))%1.

From ({eq h8}), we can prove that %2occura%1 is total by structural induction
and from this
({eq h7}) quickly follows.

	Since recursive definitions give rise to partial predicates,
and we don't want to use a partial predicate logic, we introduce a domain
%AP%1 of %2extended truth values%1 with characteristic predicate %2isetv%1
whose elements are ⊗T, ⊗F and %Aw%*.
There is no harm in identifying ⊗T and ⊗F with suitable Lisp atoms or
with the integers 1 and 0.
The following axioms describe
functions into or out of %AP%2.  We use the predicate %2istv%1 to test for
the honest truth values ⊗T and ⊗F. 
.item←0

B1:	%2∀p.(isetv p)%1

B2:	%2∀p.(p = T ∨ p = F ∨ p = %Aw%2)%1

B3:	%2T ≠ F ∧ T ≠ %Aw%* ∧ F ≠ %Aw%1

B4:	%2∀p.(istv p ≡ p = T ∨ p = F)%1

B5:	%2∀p. isetv not p%1

B6:	%2∀p q. isetv(p and q)%1

B7:	%2∀p q. isetv(p or q)%1

B8:	%2∀p.(not p =
qif (p = %Aw%*) qthen %Aw%* qelse qif p = T qthen F qelse T)%1

B9:	%2∀p q.(p and q =
qif (p = %Aw%*) qthen %Aw%* qelse qif p = T qthen q qelse F)%1

B10:	%2∀p q.(p or q =
(qif p = %Aw%*) qthen %Aw%* qelse qif p = T qthen T qelse q)%1

B11:	%2∀X Y.(X equal Y = qif ¬issexp X ∨ ¬issexp Y qthen %Aw%* qelse qif
X = Y qthen T qelse F)%1

B12:	%2∀X.(aatom X =
qif ¬issexp X qthen %Aw%* qelse qif qat X qthen T qelse F)%1,

and we also need a conditional expression that can take an argument from %AP%1,
namely

B13:	%2∀p X Y.(if(p,X,Y) = qif p = %Aw%* qthen %Aw%* qelse qif p = T qthen X
qelse Y)%1.

	%2occura%1 is proved total by applying schema LS1 with
%2%AF%*(y) ≡ occura(x,y) ≠ %Aw%*%1.  After this %2occur%1 can be shown to
satisfy ({eq h7}).

	The axioms L1-L16 and B1-B12 together with the sentences arising
from the schemata LS1 and LS2 will be called the axiom system Lisp0.  We
will adjoin one more axiom later to get the system Lisp1.

	The above method of replacing a recursion by a first order
sentence was first (I think) used in (Cartwright 1977).  I'm
surprised that it wasn't invented sooner.

.skip 1
.indent 0,0;
.bb "#. An Extended Example."

	The SAMEFRINGE problem is to write a program that efficiently
determines whether two S-expressions have the same fringe, i.e. have
the same atoms in the same order.  (Some people omit the qnils at the ends
of lists, but we will take all atoms).  Thus
((A.B).C) and (A.(B.C)) have the same fringe, namely (A B C).  The
object of the original problem was to program it using a minimum of 
storage, and it was conjectured that co-routines were necessary to
do it neatly.  We shall not discuss that matter here - merely the
correctness of one proposed solution.

	The relevant recursive definitons are

!!n1:	%2fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x%1,

where %2u_*_v%1 denotes the result of appending the lists ⊗u and ⊗v and
is defined recursively by

!!n2:	%2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1.

We are interested in the condition %2fringe x = fringe y%1.

	The function to be proved correct is %2samefringe[x,y]%1 defined by
the simultaneous recursion

!!n3:	%2samefringe[x, y] ← (x = y) ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]%1,

!!n4:	%2same[x, y] ← (qa x = qa y) ∧ samefringe[qd x, qd y]%1,

where

!!n5:	%2gopher x ←  qif qat qa x qthen x qelse gopher qaa x . [qda x . qd x]%1.

	We need to prove that %2samefringe%1 is total and

!!n6:	%2∀xy.(samefringe[x,y] ≡ fringe x = fringe y)%1.

	The minimization schemata of these functions are irrelevant, because
we will prove that the functions are all total except that we won't
prove anything about the result of applying %2gopher%1 to an atom.  The
functional equations are


!!n7:	%2∀x.(fringe x = qif qat x qthen <x> qelse fringe qa x * fringe qd x%1),

!!n8:	%2∀u v.(u * v = qif qn u qthen v qelse qa u . [qd u * v])%1.

!!n9:	%2∀x y.(samefringe[x, y] = x equal y
or [not aat x and not aat y and same[gopher x, gopher y]])%1,

!!n10:	%2∀x y.(same[x, y] = qa x equal qa y and samefringe[qd x, qd y]%1,

!!n11:	%2∀x.(gopher x =  qif qat qa x qthen u
qelse gopher qaa x . [qda x . qd x])%1.

Note that because ⊗samefringe and ⊗same are recursively defined predicates
which have not been proved total, their functional equations must use the
imitation propositional functions involving the extended truth values.

	We shall not give full proofs but merely the induction predicates
and a few indications of the algebraic transformations.  We begin with
a lemma about %2gopher%1.

!!n12:	%2∀x y.(issexp gopher[x.y] ∧ qat qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1.

	This lemma can be proved by S-expression structural induction
using the predicate

!!n13:	%2P(x) ≡ ∀y.ok(x,y)%1,

where %2ok(x,y)%1 is defined by

!!n13a:	%2∀x y.(ok(x,y) ≡ issexp gopher[x.y] ∧ qat qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1.

In the course of the proof, we use the associativity of * and the
formula %2fringe[x.y]_=_fringe_x_*_fringe_y%1.
The lemma was expressed using %2gopher[x.y]%1 in order to avoid
considering atomic arguments for %2gopher%1, but it could have
equally well be proved about %2gopher_x%1 with the condition
%2¬qat_x%1.

	Another proof can be given using the course-of-values induction
schema for integers.  We write this schema

ICV:	%2∀n.(∀m.(m < n ⊃ P(m)) ⊃ P(n)) ⊃ ∀n.P(n)%1,

.turn on "↑";
where ⊗m and ⊗n range over non-negative integers.  Exactly the same
schema expresses transfinite induction; we need only imagine the
variables ranging over all ordinals less than a given one - in this
case qw, but equally well qw%A↑w%1 or ε%40%1.
We also use the function %2size_x%1 defined by

!!n14:	%2size x ← qif qat x qthen 1 qelse size qa x + size qd x%1

satisfying the obvious functional equation.
Our induction predicate is then

!!n15:	%2P(n) ≡ ∀x y.(size x = n ⊃ ok(x,y))%1.

	
	For our proof about %2samefringe%1 we need one more lemma
about %2gopher%1, namely

!!n16:	%2∀x y.(size gopher[x.y] = size[x.y]%1.

	This can be proved by either of the above inductive methods or
by including %2size_gopher[x.y]_=_size[x.y]%1 in the induction hypothesis
%2ok[x,y]%1.

	The statement about samefringe is

!!n17:	%2∀x y.(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x =
fringe y)%1,

and it is most easily proved by induction on %2size_x_+_size_y%1 using
the predicate

!!n18:	%2P(n) ≡ ∀x y.(n = size x + size y ⊃ issexp samefringe[x,y] ∧
(samefringe[x,y] = T ≡ fringe x = fringe y))%1.

It can also be proved using the well-foundedness of lexicographic ordering
of the list %2<x qa x>%1, but then we must decide what lexicographic orderings
to include in our axiom system.

	Transfinite induction is also useful, and can be illustrated
with a variant %2samefringe%1 that does everything in one complicated
recursive definition, namely

!!n19:	%2samefringe[x,y] = (x equal y) or not aat x and not aat y and
[qif qat qa x qthen [qif qat y qthen qa x equal qa y and
samefringe[qd x, qd y] qelse samefringe[x, qaa y . [qda y . qd y]]]
qelse samefringe[qaa x . [qda x .qd x], y]%1.

The transfinite induction predicate then has the form

!!n20:	%2P(n) ≡ ∀x y.[n = qw(size x + size y) + size qa x + size qa y ⊃
issexp samefringe[x,y] ∧ (samefringe[x,y] = T ≡ fringe x = fringe y)]%1,

where in this formula qw denotes the least transfinite ordinal.

	We would like to prove that the amount of storage used in the
computation of %2samefringe[x,y]%1 aside from that occupied by ⊗x and ⊗y 
never exceeds the sum of the numbers of %2car%1s required to reach
corresponding atoms in ⊗x and ⊗y.  Unfortunately, we can't even express
that fact, because we are axiomatizing the programs as functions,
and the amount of storage used does not depend merely on the function
being computed; it depends on the method of computation.  We may regard
such things as %2intensional%1 properties, but the correspondence with
intensional properties in intensional logic remains to be established.
.bb "#. The Minimization Schema."

	The functional equation of a program doesn't completely
characterize it.  For example, the program

!!h9a:	%2f1 x ← f1 x%1

leads to the sentence

!!h10:	%2∀x.(f1 x = f1 x)%1

which provides no information although the function ⊗f 
is undefined for all ⊗x.  This is not always the case, since
the program

!!h11:	%2f2 x ← (f2 x).qnil%1

has the functional equation

!!h12:	%2∀x.(f2 x = (f2 x).qnil)%1.

from which %2∀x.¬issexp f2(x)%1 can be proved by induction.

	In order to characterize recursive programs, we need some
way of asking for the least defined solution of the functional equation.

	Suppose the program is

!!h13:	%2f x ← %At%*[f](x)%1

yielding the functional equation

!!h14:	%2∀x.(f x = %At%*[f](x)%1.

The %2minimization schema%1 is then

!!h15:	%2∀x.(isD %At%*[%Af%*](x) ⊃ %Af%* x = %At%*[%Af%*](x)) ⊃ ∀x.(isD f x ⊃ %Af%* x = f x)%1,

where the predicate %2isD%1 asserts that its argument is in the domain %2D%1.

	In the %2subst%1 example, the schema is

!!h16:	%2∀x y z.(issexp (qif qat z qthen (qif z = y qthen x qelse z)
qelse %Af%*(x,y,qa z).%Af%*(x,y,qd z)) ⊃ (%Af%*(x,y,z) = qif qat z qthen
(qif z = y qthen x qelse z) qelse %Af%*(x,y,qa z).%Af%*(x,y,qd z))) ⊃
∀x y z.(issexp subst(x,y,z) ⊃ %Af%*(x,y,z) = subst(x,y,z))%1.

	In the schema %Af%* is a free function variable of the appropriate
number of arguments.  The schema is just a translation into first order
logic of Park's (1970) theorem

!!h17:	%2%Af%* %8d%2 %At%*[%Af%*] ⊃ %Af%* %8d%2 Y[%At%*]%1.

	The simplest application of the schema is to show that the ⊗f1 
defined by ({eq h9a}) is never an S-expression.  The schema becomes

!!h18:	%2∀x.(issexp %Af%* x ⊃ %Af%* x = %Af%* x) ⊃ ∀x.(issexp f1 x ⊃ %Af%* x = f1 x)%1,

and we take

!!h19:	%2%Af%* x = %Aw%*%1.

The left side of ({eq h18}) is identically true, and, remembering that %Aw%*
is not an S-expression, the right side tells us that %2f1 x%1 is never
an S-expression.

	The minimization schema can sometimes be used to show partial
correctness.  For example, the well known 91-function is defined by
the recursive program over the integers

!!h20:	%2f91 x ← qif x > 100 qthen x - 10 qelse f91 f91(x + 11)%1.

The goal is to show that

!!h22:	%2∀x.(f91 x = qif x > 100 qthen x - 10 qelse 91%1.

We apply the minimization schema with

!!h21:	%2%Af%* x ← qif x > 100 qthen x - 10 qelse 91%1,

and it can be shown by an explicit calculation without induction that
the premiss of the schema is satisfied, and this shows that ⊗f91, 
whenever defined has the desired value.

	The method of recursion induction (McCarthy 1963) is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program on
whereever the function is defined.

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  f1 and f91 were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.

	({eq h15}) can be regarded as an axiom schema involving
a second order function variable %At%1.  What can be substituted
for %At%1 is a  quantifier free
λ-expression in a first order function variable.
It may be interesting to study the sets of first order sentences that
can be generated by such second order sentence schemata.  Presumably,
sets of sentences can be generated in this way that cannnot be
generated by schemata with only first order function variables.
.skip 1
.bb "#. Proof Methods as Axiom Schemata"

	Representing recursive definitions in first order logic permits
us to express some well known methods for proving partial correctness
as axiom schemata of first order logic.

	For example, suppose we want to prove that if the input ⊗x of a
function ⊗f defined by

!!c1:	%2f x ← qif p x qthen x qelse f h x%1

satisfies %2%AF%2(x)%1, then if the function terminates, the output %2f(x)%1
will satisfy %AY%2(x,f(x))%1.  We appeal to the following %2axiom schema of
inductive assertions%1:

!!c2:	%2∀x.(%AF%2(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ qif p x qthen %AY%2(x,y)
qelse q(x,%8 %2h y))
.nofill
		⊃ ∀x.(%AF%2(x) ∧ isD f x ⊃ %AY%2(x,f x))%1

.fill
where %2isD f x%1 is the assertion that %2f(x)%1 is in the nominal
range of the function definition, i.e. is an integer or an S-expression
as the case may be, and asserts that the computation terminates.
In order to use the schema, we must invent a suitable predicate %2q(x,y)%1,
and this is precisely the method of inductive assertions.
The schema is valid for all predicates %AF%1, %AY%1, and %2q%1, and a
similar schema can be written for any collection of mutually recursive
definitions that is iterative.

	The method of %2subgoal induction%1 for recursive programs
was introduced in
(Manna and Pnueli 1970), but they didn't give it a name.
Morris and Wegbreit (1977) name it, extend it,
and apply it to Algol-like programs.
Unlike %2inductive assertions%1, it isn't
limited to iterative definitions.  Thus, for the
recursive program

!!c3:	%2f%45%2 x ← qif p x qthen h x qelse g1 f%45%2 g2 x%1,

where ⊗p is assumed total, we have

!!c4:	%2∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
∀x.(%AF%2(x) ∧ q(x,z) ⊃ %AY%2(x,z))
.nofill
		⊃ ∀x.(%AF%2(x) ∧ isD(f(x)) ⊃ %AY%2(x,f(x)))%1
.fill

	We can express these methods as axiom schemata,
because we have the predicate %2isD%1 to express termination.
The minimization schema itself can be proved by subgoal induction.
We need only take %2%AF%2(x)_≡_%3true%1 and %AY%2(x,y)_≡_(y_=_%Af%2(x))%1
and %2q(x,y)_≡_(y_=_%Af%2(x))%1.

	General rules for going from a recursive program to what amounts
to the subgoal induction schema are given in
(Manna and Pnueli 1970) and (Morris and Wegbreit 1977);
we need only add a conclusion involving
the %2isD%1 predicate to the Manna's and Pnueli formula %2W%4P%1.
It isn't a schema in %At%1 in the form they give.

	However, we can characterize subgoal induction
as an axiom schema.  Namely, we define %At%2'[q]%1 as an extension of %At%1
mapping relations into relations.  Thus if

!!c5:	%2%At%2[f](x) = qif p x qthen h x qelse g1 f g2 x%1,

we have

!!c6:	%2%At%2'[q](x,y) ≡ qif p x qthen (y = h x) qelse ∃z.(q(g2 x,z) ∧ y = g1 z)%1.

In general we have

!!c7:	%2∀xy.(%At%2'[q](x,y) ⊃ q(x,y)) ⊃ ∀x.(isD f x ⊃ q(x,f x))%1,

from which the subgoal induction rule follows immediately given the properties
of %AF%1 and %AY%1.  I am indebted to Wolfgang Polak (oral communication)
for help in elucidating this relationship.

%3WARNING%1: The rest of this section is still somewhat conjectural
and is subject to change.  There may be bugs.

	The extension %2qt'[q]%1 can be determined as follows:
Introduce into the logic the notion of a %2multi-term%1 which is formed in
the same way as a term but allows relations written as functions.
For the present we won't interpret them but merely give rules for
introducing them and subsequently eliminating them again to get
an ordinary formula.  Thus
we will write ⊗q<e> where ⊗e is any term or multi-term.  We then form %2qt'[q]%1
exactly in the same way %2qt[f]%1 was formed.  Thus for the 91-function
we have

!!c8:	%2qt'[q](x) = qif x>100 qthen x-10 qelse q<q<x+11>>%1.

The pointy brackets indicate that we are "applying" a relation.
We now evaluate %2qt'[q](x,y)%1 formally as follows:

!!c9:	%2qt'[q](x,y)	≡ (qif x>100 qthen x-10 qelse q<q<x+11>>)(y)

			≡ qif x>100 qthen y = x-10 qelse q(q<x+11>,y)

			≡ qif x>100 qthen y = x-10 qelse ∃z.(q(x+11,z) ∧
q(z,y))%1.

This last formula has no pointy brackets and is just the formula that would
be obtained by Manna and Pnueli or Morris and Wegbreit.  The rules are
as follows:

	(i) %2qt'[q](x)%1 is just like %2qt[f](x)%1 except that ⊗q replaces
⊗f and takes its arguments in pointy brackets.

	(ii) an ordinary term ⊗e applied to ⊗y becomes %2y_=_e%1.

	(ii) %2q<e>(y)%1 becomes %2q(e,y)%1.

	(ii) %2P(q<e>)%1 becomes %2∃z.q(e,z)_∧_P(z)%1 when
%2P(q<e>)%1 occurs positively in %2qt'[q](x,y)%1 and becomes
%2∀z.q(e,z)_⊃_P(z)%1 when the occurrence is negatve.
It is not evident what independent semantics should be given to
multi-terms.
.skip 2
.bb "#. Representations Using Finite Approximations."

	Our second approach to representing recursive programs
by first order formulas goes back to Goedel (1931, 1934) who showed
that primitive recursive functions could be so represented.  (Our
knowledge of Goedel's work comes from (Kleene 1951)).

.turn on "α"
.eq←0
	Kleene (1951) calls a function ⊗f %2representable%1 if there
is an arithmetic formula ⊗A with free variables ⊗x and ⊗y such
that

!!b1:	%2∀x_y.((y_=_f(x))_≡_A)%1,

where an arithmetic formula is built up from integer constants and
variables using only addition, multiplication and bounded quantification.
Kleene showed that all partial recursive functions are representable.
The proof involves Goedel numbering possible computation sequences
and showing that the relation between sequences and their elements
and the steps of the computation are all representable.

	In Lisp less machinery has to be built up, because sequences
are Lisp data, and the relation between a sequence and its elements
is given by basic Lisp functions and by the %2subexpression relation%1
defined by

!!b2:	%2x subexp y ← (x = y) ∨ ¬qat y ∧ [x subexp qa y ∨ x subexp qd y]%1.

	%2subexp%1 is the only recursive definition we shall require.
Since it is total, we only need its functional equation to represent
it in first order logic.  The functional equation is

L17:	%2∀x y.(x subexp y ≡ (x=y) ∨ ¬qat y ∧ (x subexp qa y ∨ x subexp qd y))%1,

	The axiom system consisting of L1-L17, B1-B12, and the sentences
resulting from the schemata LS1 and LS2 will be called the axiom system
Lisp1.

	Starting with %2subexp%1 and the basic Lisp functions and
predicates we will define three other Lisp predicates without recursion.
By %2u_istail_v%1 we mean that ⊗u can be obtained from ⊗v by repeated
%2cdr%1s.  Thus the tails of (A B C D) are (A B C D), (B C D), (C D),
(D) and NIL.  The natural recursive definition of %2istail%1 is

!!b3a:	%2u istail v ← (u = v) ∨ (¬qn v ∧ u istail qd v)%1

which according to the previous sections would lead to the first order
formula

!!b3b:	%2∀u v.(u istail v ≡ (u = v) ∨ (¬qn v ∧ u istail qd v))%1,

but ({eq b3b}) is still an implicit definition of %2istail%1, because
the function being defined occurs on both sides of the equivalence
sign.  A suitable explicit definition is

!!b3:	%2∀u v.(u istail v ≡ u subexp v ∧ ∀x.(u subexp x ∧ x subexp v
⊃ x = u ∨ u subexp qd x))%1.

Next we shall define membership in a list.  We have

!!b4:	%2∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = qa u))%1.

Now we define an %2a-list%1 - a familiar Lisp concept.  We have

!!b5:	%2∀w.(isalist w ≡ ∀x.(x ε w ⊃ ¬qat x) ∧ ∀u1 u2.(u1 istail w ∧
u2 istail w ∧ qaa u1 = qaa u2 ⊃ u1 = u2))%1.

Thus an %2a-list%1 is a list of pairs such that no S-expression is the
first element of two different pairs.  Therefore, a-lists are suitable for
representing finite lists of argument-value pairs for partial functions.

	Finally, we need the familiar Lisp function %2assoc%1 that is used
for looking up atoms on %2a-lists%1.  Its familiar recursive definition
is

!!b6:	%2assoc(x,w) ← qif qn w qthen qnil qelse qif x = qaa w qthen qa w
qelse assoc(x,qd w)%1,

but it can be represented by

!!b7:	%2∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = qa w1)
∨ assoc(x,w) = qnil)%1.

	Now let ⊗f be an arbitrary recursive program defined by

!!b8:	%2f x ← %At%*[f](x)%1

for some continuous functional qt.
In order to emphasize the parallel between a partial function %2f%1 and
an %2a-list%1 used as a finite approximation, we define

!!b8a:	%At%2'(w)(x) = %At%2[λz.qif qn assoc(z,w) qthen %Aw%2
qelse qd assoc(z,w)](x)%1.

Thus %At%1' is like %At%1 except that whenever %At%1 evaluates its functional
argument ⊗f at some value ⊗z, %At%1' looks up ⊗z on the a-list ⊗w. 

	With this preparation we can write

!!b9:	%2∀x y.(y = f(x) ≡ ∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1))) ∨ f(x) = %Aw%2)%1.

	The essence of this formula is simple.  ⊗w is an a-list
containing all argument-value pairs that arise in the evaluation of ⊗f(x). 
We require that if ⊗x occurs somewhere on ⊗w, the pairs involved in the
evaluation of ⊗f(x) occur further on in the a-list ⊗w.  This is to avoid
allowing circular recursions.  If there is no such a-list, then
%2f(x)_=_%Aw%1.

	If the logic has a description operator %Ai%1, where
%Ai%2 x.P(x)%1 stands for the "the unique ⊗x such that ⊗P(x) if
there is such a unique ⊗x and otherwise %Aw%1", then ({eq b9}) can
be written

!!b9a:	%2∀x.(f(x) = %Ai%2 y.∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1))))%1.

	As an example, consider the Lisp function %2ff%1 defined
recursively by

!!b10:	%2ff x ← qif qat x qthen x qelse ff qa x%1.

({eq b9a}) then takes the form

!!b11:	∀x.(ff x = %Ai%2y.∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = qif qat x1 qthen x1 qelse (qif qn assoc(x1,qd w1)
qthen %Aw%2 qelse qd assoc(x1,qd w1)))))%1.

	Suppose we were computing %2ff_((A.B).C)%1.  A suitable ⊗w would
be ((((A.B).C).A) ((A.B).A) (A.A)).

	It might be asked whether %2subexp%1 is necessary.  Couldn't we
represent recursive programs using just %2car, cdr, cons%1 and %2atom%1?
No, for the following reason.
Suppose that the function ⊗f is representable using only the basic Lisp
functions without %2subexp%1, and consider the sentence

!!b12:	%2∀x.issexp_f(x)%1,

asserting the totality of ⊗f. 
Using the representation, we can write ({eq b12}) as a sentence
involving only the basic Lisp functions and the constant qw.
However, as is shown in Appendix I, these sentences are decidable,
and totality isn't.  (I'll put the proof in Appendix I if I can
prove it.  At this time, I think I've almost got it).

	In case of functions of several variables,
({eq b9}) corresponds to a call-by-value
computation rule while the representations of the previous sections correspond
to call-by-name or other "safe" rules.  The difference is not important, because
of Vuillemin's theorem that any strict function may be computed either according
to call-by-name or call-by-value.
.BB "#. Questions of Incompleteness."

	Luckham, Park and Paterson (1970) have shown that whether a
program schema diverges for every interpretation, whether it diverges
for some interpretation, and whether two program schemas are equivalent
are all not even partially solvable problems.  Manna (1974) has a
thorough discussion of these points.  In view of these results, what
can be expected from our first order representations?

	First let us construct a Lisp computation that does not terminate,
but whose non-termination cannot be proved from the axioms Lisp1 within
first order logic.  We need only program a proof-checker for first order
logic, set it to generate all possible proofs starting with the axioms Lisp1,
and stop when it finds a proof of (qnil ≠ qnil) or some other contradiction.
Assuming the axioms are consistent, the program will never find such a
proof and will never stop.  In fact, proving that the program will never
stop is precisely proving that the axioms are consistent.  But Goedel's
theorem asserts that axiom systems like Lisp1 cannot be proved consistent
within themselves.
All the known cases of terminating computations that
can't be proved not to terminate within Peano arithemtic
involve such an appeal to Goedel's theorem
or similar unsolvability arguments.

	We can presumably prove Lisp1 consistent
just as Gentzen proved arithmetic consistent - at the price of introducing
a new axiom schema that allows induction up to the transfinite ordinal
ε%40%1.  Proving the new system consistent would require induction up to
a still higher ordinal, etc.

	Since every recursively defined function can be defined explicitly,
any sentence involving such functions can be replaced by an equivalent
sentence involving only %2subexp%1 and the basic Lisp functions.
The theory of subexp and these functions has a standard model, the
usual S-expressions and many non-standard models.  We "construct"
non-standard models in the usual way by appealing to the theorem that
if every finite subset of a set ⊗S of sentences of first order logic
has a model, then ⊗S has a model.
For example, take %2S = α{qnil subexp x, %1(A)%2 subexp x, %1(A A)%2
subexp x, ...%1 indefinitelyα}.  Every finite subset of ⊗S has a model;
we need only take ⊗x to be the longest list of A's occurring in the
sentences.
Hence there is a model of the Lisp axioms in which ⊗x has all lists
of A's as subexpressions.  No sentence true in the standard model
and false in such a model can be proved from the axioms.  However,
it is necessary to be careful about the meaning of termination of a
function.  In fact, taking successive %2cdr%1s of such an ⊗x would
never terminate, but the sentence whose %2standard interpretation%1
is termination of the computation is provable from Lisp1.

	The practical question is: where does the correctness of ordinary
programs come in?  It seems likely that such statements will be provable
with our original system of axioms.  It doesn't follow that the system
Lisp1 will permit convenient proofs, but probably it will.  The heuristic
evidence for this comes from (Cohen 1965).  Cohen presents two systems
of axiomatized arithmetic Z1 and Z2.  Z1 is ordinary Peano arithmetic with
an axiom schema of induction, and Z2 is an axiomatization of hereditarily
finite sets of integers.  Superficially, Z2 is more powerful than Z1, but
because the set operations of Z2 can be represented in Z1 as functions
on the Goedel numbers of the sets, it turns out that Z1 is just as powerful
once the necessary machinery has been established.  Because sets and lists
are the basic data of Lisp1, and sets are easily represented, the power of Lisp1
will be approximately that of Z2, and convenient proofs of correctness
statements should be possible.  It would be nice to be able to express these
considerations less vaguely.
.bb "#. References."

%3Cartwright, R.S. (1977)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cohen, Paul (1966)%1: %2Set Theory and the Continuum Hypothesis%1,
W.A. Benjamin Inc.

%3Cooper, D.C. (1969)%1: "Program Scheme Equivalences and Second-order
Logic", in B. Meltzer and D. Michie (eds.), %2Machine Intelligence%1,
Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

%3Kleene, S.C. (1951)%1: %2Introduction to Metamathematics%1,
Van Nostrand, New York.

%3Luckham, D.C., D.M.R.Park, and M.S. Paterson (1970)%1: "On Formalized
Computer Programs", %2J. CSS%1, %34%1(3): 220-249 (June).

%3Manna, Zohar and Amir Pnueli (1970)%1: "Formalization of the Properties
of Functional Programs", %2J. ACM%1, %317%1(3): 555-569.

%3Manna, Zohar (1974)%1: %2Mathematical Theory of Computation%1,
McGraw-Hill.

%3Manna, Zohar, Stephen Ness and Jean Vuillemin (1973)%1: "Inductive Methods
for Proving Properties of Programs", %2Comm. ACM%1,%316%1(8): 491-502 (August).

%3Morris, James H., and Ben Wegbreit (1977)%1: "Program Verification
by Subgoal Induction", to appear.

%3Park, David (1969)%1: Fixpoint Induction and Proofs of Program
Properties", in %2Machine Intelligence 5%1, pp. 59-78, Edinburgh
University Press, Edinburgh.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
FIRST.NEW[W77,JMC]
PUBbed at {time} on {date}.%1